open time
open util/boolean

/**--------------------**/
/** User Classes **/
/**--------------------**/

abstract sig  User
{
}

sig Guest extends User{}

sig RegisteredUser extends User
{
	isLogged: Date -> one Bool,
	abilities: set Ability,
	feedback: set Feedback,
	receivedMessages: set Message,
	sentMessages: set Message,
	friends: set RegisteredUser,
	indirectFriends: set RegisteredUser
}
{
	indirectFriends in friends
}

sig BannedUser extends RegisteredUser
{
	endBan: Date
}

sig Admin extends RegisteredUser{}

one sig Founder extends Admin{}

/**-----------------------**/
/** Object Classes **/
/**-----------------------**/

abstract sig Object
{
	creationDate: Date
}

sig Message extends Object
{
	sender: User,
	recipient:set RegisteredUser,
}

sig Ability extends Object
{
}

sig Feedback extends Object
{
	leftBy: one RegisteredUser,
	inResponseOf: one HelpRequest
}
{
	leftBy = inResponseOf.generatedBy
}

sig HelpRequest extends Object
{
	expiredate: Date,
	generatedBy: one User,
	involves: one RegisteredUser
}

/**----------**/
/** Facts **/
/**----------**/

/**HelpRequest**/

//every request involves exactly two user, the genarator and the recepient.
//The generator can be a guest, the recipient can be a RegisteredUser only
fact involesTwoUser
{
	all hr: HelpRequest | one ru:RegisteredUser, u:User
	{
		hr.generatedBy = u && hr.involves = ru
	}	
}

//no self help requests
fact noSelfRequest
{
	all hr: HelpRequest | no u:User
	{
		u = hr.involves && u = hr.generatedBy
	}
}


//Same request can't come from two different users
assert noSameHelpFromTwoUser
{
	all hr:HelpRequest | no u: User, u1:User
	{
		hr.generatedBy = u && hr.generatedBy = u1 && u != u1
	}
}

//The same help can't be given to two different user
assert noSameHelpToTwoUser
{
	all hr:HelpRequest | no u: User, u1:User
	{
		hr.involves = u && hr.involves = u1 && u != u1
	}
}


/** messages **/
//The recipient of a message must have it in their inbox
fact MessageInReceivedMessages
{
	all m: Message | m in m.recipient.receivedMessages 
}


//I receive only my messages
fact ReceiveMyMessage
{
	all ru:RegisteredUser | #ru.receivedMessages >0 implies ru.receivedMessages.recipient = ru		
}

//if the sender is registered then he has the message in his outbox and vice versa
fact MessageInSentMessages
{
	all ru: RegisteredUser | #ru.sentMessages >0 implies ru.sentMessages.sender = ru
}

fact onlyRecipientGetMessage
{
	all ru: RegisteredUser | #ru.receivedMessages >0 implies ru in ru.receivedMessages.recipient
}

//All the messages are in the outbox of a registered user or they are sent by a guest
fact noIslandMessage
{
	all m:Message
	{
		(one g:Guest | m.sender = g) or (one ru:RegisteredUser | m in ru.sentMessages)  
	}
}

//Banned user can't send messges
fact LonelyBanned
{
	all m: Message | m.sender not in BannedUser
}

/** friends **/

fact FriendOfMyFriend
{
	all ru',ru'': RegisteredUser 
	{ 
		(ru'' in ru'.friends iff ru' in ru''.friends) &&  
		(ru'' in ru'.indirectFriends iff ru' in ru''.indirectFriends)
	}
}

fact noSelfFriends
{
	no ru: RegisteredUser
	{
		ru in ru.friends
	}
}

/** Feedback**/

fact noSelfFeedbacks
{
	all ru: RegisteredUser
	{
		no f: Feedback | f.leftBy = ru && f in ru.feedback
	}
}

fact noFeedbackIsland
{
	all f: Feedback 
	{
		one ru: RegisteredUser |  f in ru.feedback
	}
}

fact HelpBeforefeedback
{
	all f: Feedback
	{
		gte[f.creationDate,f.inResponseOf.expiredate]
	}
}

fact NoDoubleFeedBack
{
	no f,f':Feedback
	{
		f!=f' && f.inResponseOf = f'.inResponseOf
	}
}

fact NoBannedFeedBack
{
	no f:Feedback
	{
		f.leftBy in BannedUser 
	}
}

/**------------------**/
/**  Predicates **/
/**-----------------**/

pred show
{
	#Feedback > 0
}

pred guestSentMessageShow[g:Guest, m:Message] 
{
	some ru: RegisteredUser | m in ru.receivedMessages && m.sender = g
}

pred showFriends
{
	some u: RegisteredUser | #u.friends = 6 && #u.indirectFriends = 4
}

pred noMessages
{
	#Message =0
}

pred showBanned
{
	#BannedUser > 0
}

pred showHelpRequest
{
	#HelpRequest > 0
}

pred showLogin
{
	#HelpRequest= 0  && #Ability = 0 && #Message = 0 && #BannedUser = 0
}
/**  Assert **/

assert WrongMessages
{
	some u: RegisteredUser | u not in u.receivedMessages.recipient
}

assert noMessageAlone
{
	no m:Message | no ru:RegisteredUser | m.sender = ru implies m in ru.sentMessages
}

//All and only recipients receive their messages
assert RecipientInboxMismatch
{
	all m: Message | m in m.recipient.receivedMessages && no u: User 
	{
		m in u.receivedMessages &&  not(u in m.recipient) 
	}
}

//Only  the sender has the message in his outbox
assert SenderOutboxMismatch
{
	all m: Message | m in m.sender.sentMessages implies no ru: RegisteredUser 
	{
		m in ru.sentMessages &&  ru != m.sender 
	}		
}

//Feedbacks are sent by the person who ask for the help
assert OnlyHelpedCanFeedback
{
	all f:Feedback
	{
		f.leftBy = f.inResponseOf.generatedBy
	}
}




/**-----------------------------**/
/** Execution Comands **/
/**-----------------------------**/

check noSameHelpFromTwoUser for 5

check noSameHelpToTwoUser for 5

check noMessageAlone for 5

check SenderOutboxMismatch for 10
 
check RecipientInboxMismatch for 5

check OnlyHelpedCanFeedback for 10

run guestSentMessageShow for 5

run showFriends for 10

run showHelpRequest for 5

run showBanned for 10

run showLogin for 4

run noMessages for 5

run show for 5
